Inference at * 1 1 1 1 
Iof proof for Lemma fseg extend:



1. T : Type
2. l1 : T List
3. v : T
4. l2 : T List
5. L : T List
6. l2 = (L @ l1)
7. ||l1|| < ||l2||
8. l2[(||l2|| - (||l1||+1))] = v
9. (null(L))
10. L' : T List
11. L = (L' @ [last(L)])
12. 0 < ||L||
  last(L) = (L @ l1)[(||L @ l1|| - (||l1||+1))] 

latex

 by ((((RWO "select_append_front" 0) 
CollapseTHEN (Auto'))) 
CollapseTHEN (((
CRWO "length_append" 0) 
CollapseTHEN (Auto')))) 

latex

C1: 

C1:   last(L) = L[((||L||+||l1||) - (||l1||+1))]
C.

Definitions	P  Q, , T, True, t  T, x:A. B(x), P  Q, P  Q, x:AB(x), P & Q, x:A  B(x), A  B, [car / cdr], [], last(L), l[i], n - m, n+m, #$n, as @ bs, A, a < b, type List, Type, s = t, ||as||, i  j
Lemmas	select append front, iff wf, rev implies wf, le wf, squash wf, select wf, length append